perm filename PROVER.DOC[P,JRA]1 blob
sn#026685 filedate 1973-02-28 generic text, type T, neo UTF8
Preliminary User Manual February 28, 1973
Preliminary User's Manual for the Theorem Prover
The current program is a resolution- and paramodulation-based theorem
prover with extensive facilities for on-line control. Perhaps the
easiest introduction is to follow the development of a few examples.
Example 1.
Consider the following set of statements:
(1) (∀x∀y){P(x,y) ∧ P(y z) ⊃ G(x,z)}
(2) (∀y∃x){P(x,y)}
We might interpret these statements as claiming
"For all x and y, if x is the parent of y and y is the parent
of z, then x is the grandparent of z,"
and
"Everyone has a parent."
Given these statements as hypotheses we might wish to know if there
were individuals, x and y such that x is the grandparent of y. We
could pose that question as the statement:
(3) (∃x∃y){G(x,y)}
It is clear that (3) does indeed follow from (1) and (2). How do we
formulate the problem for the theorem prover?
Here is one axiomatization:
PRE_PRED: P,G;
VAR:x,y,z;
G1: ∀(x,y)(P(x,y) ∧ P(y,z) ⊃ G(x,z));
G2: ∀y∃x P(x,y);
THEOREM: ∃(x,y)G(x,y);
;
Some of the conventions displayed in the example are:
(1) the predicate letters and function symbols must be declared
according to their type. For example infix and prefix operators are
declared by INF_OP and PRE_OP respectively. Constants are considered
Preliminary User Manual February 28, 1973
to be prefix operators of zero arguments. (2) variables must be
declared;any extra variables which are needed in outputting derived
clauses are generated from the initial variable list. For example
x1,x2,...y1,y2... . (3) each statement must be terminated with a
semi-colon; (4) statements or sets of statements may be labeled.
These labels can by used to refer to clauses in the on-line editor.
If a statement is labeled, THEOREM, then the negation of that
statement is formed and is used in the list of input statements. (5)
adjacent like quantifiers may combined. (6) the whole set of
declarations and input statements must be delimited by a semicolon.
A complete description of the syntax and semantics of the input
format is given in the appendix.
Preliminary User Manual February 28, 1973
Example 2.
In an investigation of axiomatizations of elementary group theory the
following statements arose:
(1) x*x = y*y
(2) x*(y*y) = x
(3) x*(y*z) = z*(y*x)
(4) x*(x*y) = y
(5) (x*z)*(y*z) = x*y
Question: Does (5) follow from (1)-(4)?
The answer is "yes" but it is not immediately obvious. It is more
difficult to establish than Example 1. Notice that this Example is a
pure equality formulation, requiring only replacements of terms by
other terms. This example could be presented to the prover as:
INF_OP: *;
INF_PRED: =;EQUALITY:=;
VAR: x,y,z;
AXIOMS: x*x = y*y;
x*(y*y) = x;
x*(y*z) = z*(y*x);
x*(x*y) = y;
THEOREM:(x*z)*(y*z) = x*y;
;
In this example, the name AXIOMS, refers the first four statements.
Before presenting a more complicated example, we shall describe how
to use the prover on these first Examples.
Preliminary User Manual February 28, 1973
Once the input file has been prepared you are ready to used the
theorem prover. The command: RUN PROVER [P,JRA] , will select the
current version of the program. The appearence of an asterisk (*)
signifies that the program is ready. If you wish the program to make
an initial selection of strategies for your problem then type:
(PROVE DSK: filename). The exact strategies which are chosen are
described in Section ⊗⊗⊗. if you would rather select you own
strategies then type: (TRY DSK: filename). You will then be asked to
describe your choice and editing strategies. See Section ⊗⊗⊗ for a
complete description of strategy selection.
If the (translations of) the set of input statements are found to be
inconsistent, then the sequence of deductions which exhibits that
inconsistency is displayed on the console. This refutation and the
set of strategies which were employed are also saved on a disk file .
The name of the file is created from the name of the input file.
Thus, for example, (PROVE DSK: FOO) and (PROVE DSK: (FOO.A)) would
create an output file named N1FOO.PRF. If the input initially comes
for the console using (PROVE) or (TRY), then the output file is given
the name, N1PRF.PRF. It is also possible that the prover terminate
without finding a refutation. This could occur either because the
selected strategies do not form a complete set or because the initial
set is not inconsistent. In either case the program types NO-PROOF-
FOUND and enters the clause editor to wait for commands from the
user.
Preliminary User Manual February 28, 1973
Now let's try running the first example. Assume that a disk file,
EX1, has been prepared containing the axiomatization. What follows is
a running commentary on what should occur. Material preceeded by | is
commentary; statements typed by the user are preceeded by *.
*RUN PROVER [P,JRA] |retrieve the current prover.
*(PROVE DSK: EX1) |Request that the program pick the
|strategies while running EX1.
PRE_PRED: P,G; |The program is accepting the axioms.
VAR: x,y,z;
G1:
∀(x,y)(P(x,y) ∧ P(y,z)) ⊃ G(x,z));
G2:
∀y∃x P(x,y);
THEOREM:
∃(x,y)G(x,y);
HERE-ARE-THE-CLAUSES: |What follows are the translations
|of the input into clause-form, with
1 P(x,z)∧P(y,z) ⊃ G(x,y) |the redundant statements removed.
2 P(G21(x),x) |G21 is a generated Skolem function.
3 ¬G(x,y) |The translation of the negation of
|the theorem.
4 ¬(P(z,x)∧P(x,y)) |A deduction which has been added to
|the list of clauses.
COUNT = 1 |There was only one resolvent formed
LEVEL = 1 |on level one.
ELAPSED-TIME = 333 |The execution time in milliseconds.
5 ¬P(x,y);
COUNT = 3
LEVEL = 2 |Three resolvents have been formed by
ELAPSED-TIME = 500 |the end of level 2. (Two have been
|retained.)
NIL 1 4 |A contradiction. These next six
1 -P(x,y) 3 4 |lines are the refutation. I.e.:
3 ¬(P(z,x)∧P(x,y)) 5 6 | 6 5
4 P(G21(x),x) G2 | \ /
5 P(x,z)∧P(y,z) ⊃ G(x,y) G1 | 3 4
6 ¬G(x,y) THEOREM | \ /
| 1 4
| \ /
| NIL
Preliminary User Manual February 28, 1973
Notes:
1. The labeling of the input is reflected in the description
of the refutation tree. That is, P(G21(x),x) resulted from
the translation of G2; ¬G(x,y) came from the negation of the
theorem.
2. A copy of the refutation tree, relevant statistics, and a
description of the actual strategies used, now appears on a
file named #1EX1.PRF.
Preliminary User Manual February 28, 1973
Now let's run the second example. Assume that the axiomatization is
on a file named EX2.
*RUN PROVER [P,JRA]
*(PROVE DSK: EX2) |Again, let the program
|pick the strategies.
INF_OP: *;
INF_PRED: =;
EQUALITY: =;
VAR:x,y,z;
AXIOMS:
x*x=y*y;
x*(y*y)=x;
x*(y*z)=z*(y*x);
x*(x*y)=y;
THEOREM:
(x*z)*(y*z)=x*y;
HERE-ARE-THE-CLAUSES:
1 x*x=y*y
2 x*(y*y)=x
3 x*(y*z)=z*(y*x)
4 x*(x*y)=y
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2
|Again, THMn's are generated
|Skolem constants.
NIL 1 2 |An immediate contradiction
1 x=x; |We know E is reflexive
2 ¬THM1*THM2=THM1*THM2 3 4 |moderate mystery.
3 x*(y*z)=z*(y*x) AXIOMS
4 ¬(THM1*THM3)*(THM1*THM2)=THM1*THM2 THEOREM
Notes:
1. The `refutation' is a bit mysterious. A more sympathetic proof
recovery mechanism is contemplated, but perhaps some of the current
mystery can be dispelled.
A `natural' proof might be:
1. (x*z)*(y*z) = z*(y*(x*z)) replacement using (3)
2. z*(y*(x*z)) = z*(z*(x*y)) replacement using (3)
3. z*(z*(x*y)) = x*y replacement using (4)
Preliminary User Manual February 28, 1973
The above proof is indeed a translation of the machine proof.
Besides replacement, the prover also has a special rule of
simplification. Whenever an equality formulation is presented to the
prover, a list ,SL,is made consisting of all the equalities which
occur in the input. In the current example, SL would consist of
everything but the negation of the theorem. Let t1 = t2 be a member
of SL. Whenever a deduction is formed (but before it has been added
to the memory of the prover) we attempt to match t1 against terms
occurring in the deduction. If matches can be made we repalce those
terms with the appropriate instance of t2. It is this simplified
deduction which is presented to the prover.
Preliminary User Manual February 28, 1973
Thus the refutation really is:
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2 THEOREM
\
\
\ x*(y*z)=z*(y*x) AXIOMS
\ /
\ /
¬THM3*(THM2*(THM1*THM3))=THM1*THM2 by replacement
\
\
\ x*(y*z)=z*(y*x) AXIOMS
\ /
\ /
¬THM3*(THM3*(THM1*THM2))=THM1*THM2 by simplification
\
\
\ x*(x*y)=y AXIOMS
\ /
\ /
¬THM1*THM2=THM1*THM2 by simplification
\
\
\ x=x
\ /
\ /
NIL
by resolution
Preliminary User Manual February 28, 1973
Most applications of the prover lie in that gray area between a quick
proof and the occurrence of NO-PROOF. That is, an application of the
prover usually generated a large number of deductions before either a
proof is found or no more deductions can be made under the current
strategy settings. It is this area which can be profitably explored
using interactive commands. If the user sees a deduction which
should lead to the desired refutation he is able to guide the
program to the explicit contradiction. If he sees a deduction which
he feels is interesting, he can explore its consequences in the set
of statements. If he feels that the strategy settings are ill-chosen
then he can abort the current proof-search and pick new strategies.
The next sections give detailed descriptions of the current on-line
commands.
First, the on-line editor is entered by striking the space bar.
I. GENERAL BOOKEEPING COMMANDS.
CHange CH;
It is frequently desireable to change some of the
strategies while a proof attempt is in progress.
CHange describes what choice and editing strategies
are currently active and asks which are to be
changed.
CUrrent CU;
This command simply lists the current strategy
settings.
DSkout DS <filename>;
This command diverts future output to specified disk
file.
Preliminary User Manual February 28, 1973
EVal EV;
This command is mostly a debugging aid and is
included for completeness. The casual users should
not have to resort to its use. EVal enters a READ-
EVAL-PRINT. To return to the editor, type @END.
HAlt HA;
HAlt stops the prover is such a state that if the
current core image is saved, it can be continued. To
resume execution of such a core image, type RUN DSK:
name. When the asterisk appears you are in the on-
line editor. Then type TErminate.
End Of file EO;
EOf is used to terminate the DSkout command.
HElp HE;
This command will type a list of the available
editing commands along with an abbreviated
description of their action.
TErminate TE;
This command is used to terminate the editing process
and return to the prover.
Preliminary User Manual February 28, 1973
II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
Each clause which has been retained by the prover -- initial clauses
or deduction -- is given a number, the first axiom, the number 1.,
etc.. These numbers are permanently assigned, even though certain
actions of the prover may remove clauses from consideration by the
rules of inference. Clauses which have been so deleted are displayed
as *DE*. When the editor is entered, a hypothetical pointer is
initialized to the first clause. This first set of commands allow
the used to manipulate the set of clauses using the associated
numbers.
FLoat UP FU; or FL UP;
Moves the pointer up through the list of clauses.
The motion is stopped either by striking a key or by
reaching the upper extreme of the list. FLoat UP may
also be apbbreviated as FU.
FLoat DOwn FD; or FL DO;
The counterpart of FLoat UP. FLoat Down may also be
abbreviated as FD.
UP UP n;
UP is to be followed by an integer, N. The effect of
this command is to move the pointer up N clauses from
its current setting. As the pointer is moved, the
interviening clauses are printed. If N = 0, then the
pointer is immediately moved to the beginning of the
clause list. As with the FLoat commands,striking a
key will stop the pointer.
DOwn DO n;
The counterpart of UP. DOwn 0 moves the pointer to
the end of the list.
GO GO n;
Preliminary User Manual February 28, 1973
GO is to be followed by an integer designating a
clauses. The pointer goes immediately to the
designated clause.
Preliminary User Manual February 28, 1973
Though these commands have proved quite useful, experience has
shown that more global manipulation of the clauses is needed.
Therefore we have commands for assigning names to subsets of the
clause list, and commands for manipulating these sets. Just as each
element of the primary list of clauses is assigned a unique positive
integer, so is each element of each named subset. For example to
refer to the second element of the set named FOO, use FOO[2]; to
refer to the second and third elements, use FOO[2,3]. Certain
commands, like REsolve or PAramodualte create new names, like
RES1,RES2, etc. or PAR1, PAR2. These created names are local to that
call on the on-line editor. Names which were initiated by the user
using the SEt command are global.
The following BNF equations will be used in the sequel:
<clauses> ::= {<c>,}*<c>
<c> ::= <number>|<id>{[{<number>,}*<number>]}*
::= @<statment>|FIND[<id>;<pattern>]
CLear CL <id>;
CLear takes a name as argument. This command only
removes the name from the symbol table; it does not
affect the clauses attached to the name.
Delete DE <clauses>;
The designated clauses are deleted from the memory of
the prover. Attempts to display such clauses will
print *DE*. Other attempts to use deleted clauses in
editing commands will invoke an error message.
DIsplay DI <clauses>;
This command displays all the elements of <clauses>;_
Preliminary User Manual February 28, 1973
INsert IN <id> <statements>; IN <id> DSK: <file>;
This command is used to enter new clauses into the
clause editor. The first argument to INsert is a
<name>. What follows is a set of clauses, or a file
designator. If the clauses are typed they must
conform to the standard input format; if a file
designator is given, the specified file must be in
the correct format. IN is a special case of the SEt
command.
SAve SA <clauses>;
Most of the results of the on-line commands:
deductions, insertions, substitutions,etc, are local
to the clause editor. To include any of these
resulting clauses in the memory of the prover use the
Save command.
SEt SE <id> <clauses>;
SEt <id> <clauses>; has the effect of assigning to
<id>, the sequence of clauses selected by the
<clauses>. Within a particular proof attempt, the
names selected by the user are retained.
The commands listed above give us a reasonably powerful set of
instructions for manipulating the clause list. Clearly, before we can
really begin to guide the prover we must be able to perform the rules
of inference on-line. The next set of commands begins to do this.
III. COMMANDS FOR PERFORMING RULES OF INFERENCE
PAramodulate PA <clauses>; <clauses>;
This command handles equality replacements. All
equality literals of the form t1=t2, are used in
equality replacements in the following manner: let s
be any term, not a variable, which occurs in some
literal in one of the clauses. If s occurs no deeper
than PDEPTH (see the appendix for PDEPTH) and there
is a substitution unifying s and t1, then the
occurrence of t1 is replaced by the appropriate
instantiation of t2.
Preliminary User Manual February 28, 1973
REsolve RE <clauses>;<clauses>;
This command takes a pair of <clauses> as arguments.
The resolvents of these two sets are formed, a unique
name is generated and the resolvents are assigned to
that new name. The generated names are presently of
the form RESn, for some integer,n.
SImplify SImplify <clauses>; BY <clauses>;
This command is similar to the PA command. Here the
second set of clauses is to be a list of equality
units, again of the form t1=t2. Terms occuring in the
first set of clauses which unify with elements, t1,
are replaced by instances of t2. DDEPTH determines
the depth to which the match is attempted.
Example 3. A simple example of the use of the rules of inference.
Assume that R is the equality predicate and that we have just struck
a key on the console.
*DI 1,2,3; |Display the first three clauses
1 x≤y ⊃ x/y=0
2 ¬1/(a/b)=0
3 0≤x
*PA 1; 2; |Use replacement on 1 and 2.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME: PAR1 |PAR1 is a created name.
1 1≤a/b ⊃ 1=0
*PA 2; 3; |Try to use the replacement rule
NO-PARAMODULANTS |on clauses 2, and 3.
*RE 1; 3;
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:RES1 |RES1 is another created
|name.
1 0/x=0
*PA RES1; RES1; |Created names are legal.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:PAR2 |PAR2 is a new name.
1 0=0 |True.
Preliminary User Manual February 28, 1973
*SA PAR1[1]; |Add 1≤a/b ⊃ 1=0 to the memory
|of the prover;
Preliminary User Manual February 28, 1973
IV. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.
Though the commands, REsolve and PAramodulate, are useful for fine
control of the prover, is is often useful to demand larger inference
steps. That is, using some of the existing clauses in memory, with
perhaps some additional assumptions, we wish the prover to attempt to
establish the validity of a first order formula. While this subproof
is under investigation the state of the main proof should be
preserved. The commands in this section are used to initiate and
control such subproofs.
ABort AB ; or AB <clauses>;
This command is used to manually abort a proof
attempt, returning to the previous level. If
<clauses> is present, then the selected clauses are
returned and assigned to a created name.
USing US <clauses>; or US DSK: <file>;
The selected clauses are designated to be used in the
forthcoming subproof.
PRove PR <statement>; or PR DSK: <file>;
The <statement> is translated and will be attached to
the name LEMMA. The negation of the statement is also
formed and will be used in the subproof. Thus both
the positive and negative tanslates are formed. The
positive translate is maintained for the convenience
of the user since after the lemma has been
established it should be available for further
deductions. Within the subproof the negation of the
<statement> will appear under the local name, THMS.
These last two commands,--USing, and PRove -- are used to initialize
the call on the prover; USing may be omitted. There are two commands
to commence the subproof.
EXecute EX;
Preliminary User Manual February 28, 1973
EXecute begins the subproof using a computed set of
stategies.
TRy TR;
TRy first enters the strategy selection dialog, then
begins the subproof with the chosen strategies.
In both cases the strategies of the subproof are completely local.
They in no way affect the strategies in the parent proof. If a key is
struck while in the subproof the editor is entered and can manipulate
the local clauselist or initiate another subproof. The TErminate
command will comtinue the subproof, the ABort command will return to
the previous level.
Preliminary User Manual February 28, 1973
Example 3. A simple example of subproof generation.
Suppose that we have struck a key during a proof-search.
*AN 10; |Display the ancestry of
P(A) 1 2 |clause no. 10.
1 P(A) ∨ P(B) AX1
2 ¬P(B) HYP1
*USING 10, @P(A) ⊃ P(B); ; |Setup the assumptions for the
|lemma.
|Use clause no. 10 in the attempt
*PROVE @P(B);;
*EX; |This initiates the subproof.
NIL 1 2
1 P(A) DEDUCT |Clause 10 becomes an "axiom"
2 ¬P(A) 3 4 |with the subproof.
3 P(A)⊃P(B) INSERT
4 ¬P(B) THEOREM |The negation of the lemma
CONTRADICTION-FOUND-FOR-LEMMA
|We are now back in the editor
*DI 10; |Display clause no. 10.
P(A)
*DI LEMMA; |The translate of the statement
P(B) |to be PROVEed.
*USING LEMMA;
*PROVE @∃(x)P(x);; |LEMMA now becomes the translate
*EX; |this clause.
NIL 1 2
1 P(B) AX1
2 ¬P(X1) THEOREM
CONTRADICTION-FOUND-FOR-LEMMA
*DI LEMMA; |ED1 is a ubiquitous Skolem
P(ED1) |constant.
Preliminary User Manual February 28, 1973
V. COMMANDS USEFUL WHEN NO PROOF IS FOUND
When the prover is unable to make new deductions which satisfy the
current strategies it will report that no refutation can be found,
and will enter the on-line editor. At this time the user can examine
the list of clauses, perform rules of inference, initiate sub-proofs,
or use the other on-line commands. The user also has the opportunity
to save any or all of the current deductions and begin a the proof
search again, perhaps with new strategies. The user can also force a
proof attempt to be abandoned by typing AB;. This has exactly the
same effect as if the prover could make no new deductions.
ABandon AB;
AB, typed in this context (not in a subproof)
terminates the main proof attempt, enters the on-line
editor, and waits for commands.
TErminate TE <clauses>; or TE;
If <clauses> are present then they are added to the
list of clauses named THMS. The list, AXIOMS, HYPS,
and THMS are preserved and a new proof attempt is
begun. If the initial attempt was through PROVE then
the user is asked if he still wants automatic
strategy selection. If the initial attempt was
through TRY or the user does not wish automatic
selection, then a dialogue is begun describing the
current strategies and asking if changes are desired.
Then a new proof search is begun.
This use of AB and TE is useful for feeding `interesting' deductions
back into a proof search without having to restart the whole process.
The derivation tree of any such saved derived clause is maintained
for the proof recovery mechanisms but such clauses appear to be
`input' clauses to the rules of inference.
Preliminary User's Manual February 28, 1973
V. SEARCHING AND PATTERN MATCHING.
The pattern matching facilities for interactive theorem proving are
the most difficult feature to describe well. The tools presented to
the user should be general enough to significantly aid in the search
for a proof. At the same time the pattern matching commands should
be concise and somewhat readable. Clearly, pattern matching is
present throughout the theorem prover; the choice strategies, the
rules of inference, and the editing strategies are all examples of
very sophisticated pattern matching. Thus pattern matching is very
important part of the theorem proving process. Indeed we are
currently exploring a general theroem proving language which will
exploit pattern matching in all aspects of proof search -- rules,
strategies, and heuristics.
Pattern matching is invoked by the FIND operation.
FIND[<id>,<pattern>] expects <id> to be the name of a list of
clauses, and <pattern> should be a Boolean combination of primitive
patterns. These primitive patterns are completely described in the
next section, but basically allow description of syntactic parts of
clauses.
Since many of the applications of FIND are of the form
FIND[CLAUSES,<pattern>], the abbreviation, FINDC[<pattern>] has been
added for this case.
Here's an example of FIND and FINDC.
SET XX FINDC[0εC]; |C is a 'clauses variable'. The pattern says
|find all clauses in the set CLAUSES which
|have occurrences of the symbol 0.
Preliminary User's Manual February 28, 1973
|In this problem 0 is a function letter.
*
DI XX; |Display the clauses.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
3 0≤x;
4 x/x=0;
5 x/1=0;
*
SET YY FIND[XX,≤εC]; |Find all clauses in XX which have occurrence
|of the symbol '≤', and assign those clauses
|to YY.
*
DI YY; |Display YY.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
*
SET ZZ FIND[YY,/εC∧=εC];
*
SET ZZ FIND[YY,⊂/,=⊃εC];|These last two patterns have exactly the
|same effect.
*
VI. PRIMITIVE PATTERN LANGUAGE.
A simple language has been devised for more precise descriptions of
strategies than Boolean combinations of the builtin strategies. This
language is also useful for describing patterns for searching clause
lists using FIND and FINDC.
This language allows rather arbitrary functions on the syntactic
structure of clauses terms and literal.
The interpretation of the constructed formulas differs depending on
whether the formula is an editing strategy, a choice strategy, or a
pattern. Formulas to be used for choice strategies are supposed to
Preliminary User's Manual February 28, 1973
be applied to a binary rule of inference, I, in the presence of two
clauses, C1 and C2; that is, I(C1,C2). An editing strategy formula
is to be applied to a single clause, thus there should be exactly one
`clause variable', currently named C. Thus when we give choice
strategies then formula is used as a filter on each pair of
candidates. When we use the formulas on clause-lists in the editing
phase, they ae to be applied to each clause, any clause satisfying
the editing formula is to be edited out.
PRIMITIVES:
1) ancestry TR(x)
Examples:
If x is an initial clauses then TR(x) is NIL. If x is a deduction
then TR gives a list of the clauses appearing in the derivation
tree.
2) length α(x)
If x is a clause then α(x) gives the usual length--number of
literals.
Examples:
α(C1)=1 is true if C1 is a unit-clause.
3) depth ∂(x)
This gives the maximum depth of function nesting in the clause,x.
PREDICATES:
=,<,>,¬ equality,less-than,greater-than, not
∧,∨,ε and,or,clever membership.
[ p→e; ...] conditionals
Preliminary User's Manual February 28, 1973
Examples: a) ∂(C1)<5 ∧TR(C1)=NIL
Depth of nesting is less than 5 and clause is initial.
MATCHING:
+,- sign of a literal ⊂,⊃ set delimiters for
and-membership ⊃,⊂ set delimiters for or-membershit
Examples; ⊂2,3,4⊃εTR(c)
Each clause 2,3,and 4 must appear in the tree of c.
⊃2,3,4⊂εTR(c)
At least one of these clauses must appeaar.
_ matches any term
x,y,z,u,v used to match sub-terms.
Examples: f(_,_) matches any occurrence of the function-letter,f.
f(g(x,_),_,x) matches any occurrence of f such that f's first
position is an occurrence of g; and g's first position matches the
third position of f.
Examples:
Definition of some of the builtin strategies in the language.
ANCESTRY: TR(C1)=NIL ∨ TR(C2)=NIL ∨ C2εTR(C1) ∨ C1εTR(C2)
SUPPORT[...]: [TR(C2)=NIL → ⊃...⊂εTR(C2);T → T]
UNIT: α(C1)=1 ∨ α(C2)=1
VINE: TR(C1)=NIL ∨ TR(C2)=1
LENGTH[#]: α(C) > #
DEPTH[#]: ∂(C) > #
Preliminary User'Manual February 28, 1973
Frequently the user of a theorem prover "knows" a lot of detail about
the problem domain being axiomatized. Much of this information
(almost by definiton) is domain-dependent and thus doesn't fit the
usual set of strategies as well as could be desired. Also much of
this information is heuristic in nature and would be difficlut to
express in the form of axioms. To help with these problems we have
introduced two new ideas: (1) a language for describing strategies;
and (2) new data types have been added to LISP so that the user may
taylor-make his own prover.
The strategy language allows Boolean and conditional expressions over
properties of clauses. Major extensions of this idea are
contemplated..
The programmable aspects allow the user to describe first oreder
statements, strategies and pattern matching in an intuitive notation.
With these facilities inside LISP we can write new rules of inference
and domain dependent theorem provers.
Preliminary User'Manual February 28, 1973
The Language of Strategies.
(1) Choice strategies.
Choice strategies occur in the following context: Given two possible
candidates,C1 and C2, for the application of a binary rule of
inference, I, a choice strategy will determine whether not we wish to
form I(C1,C2).
Builtin choice strategies.
a) NONE allows unrestricted applications of the rules of inference.
b) ANCESTRY implements the AFF strategy; that is, to apply I either
C1 or C2 must be an initial clauses, or, either C1 appears in the
derivation tree of C2, or C2 appears in the tree of C1.
c) SUPPORT designates the set-of-support strategy. This strategy
basically says that every first-level deduction must have one of its
parents in the support set. SUPPORT must be followed by an argument
list describing which statements are to be supported. The elements
of the argument list may either be clause numbers or names which the
user has associated with certain input clauses.
Example: SUPPORT[1,2,AXIOM[2],THEOREM] would put clauses numbered 1
and 2, the clause AXIOM[2], and all clauses with name, THEOREM, in
the support set.
d) VINE strategy says that either C1 or C2 must be an initial clause.
This strategy is known to be incomplete, but is useful in many cases.
e) UNIT strategy says that either C1 or C2 are singletons. Again,
Preliminary User'Manual February 28, 1973
this strategy is not complete ,but is useful as a "quick-kill" or
"end-game" strategy. It is easy to show that if there is a UNIT-
refutation then there is a VINE-form refutation. It is also easy to
show that if all the initial statements are either units(singletons)
or are of the form L1∧L2∧...∧Ln ⊃ M then there is a UNIT proof.
f) P1 is the P1-deduction of Robinson. Here it is required that
either C1 or C2 contain only positive literals. This strategy is
complete.
g) MODEL is the implementation of a very simple case of the model-
relative deduction strategy of Luckham. Model-relative deduction is
a generalization of P1 deduction and is complete. Deduction relative
to a model says that at least one of the clauses C1 or C2 be false of
the model. MODEL expects an argument list describing a binary
partition of the predicate letters appearing in the initial clauses.
In the current restricted implementation this says either C1 or C2
must have zero intersection with the two members of the partition.
h) DEFMODEL can be used to designate a LISP function to define a
model for the current set of statements. DEFMODEL expects a single
argument which is the name of a LISP function(of one argument) and
which implements the defining conditions of a model.
i) EQUALITY signals that the replacement rule, paramodulation, is to
be used. EQUALITY needs two arguments: a predicate name to be
interpreted as equality; and second, a number, called PDEPTH, which
Preliminary User'Manual February 28, 1973
determines how deep in the nesting of function symbols the matcher
will look in attempting to match terms. For example, a PDEPTH of 1
says only examine primary occurences of terms.
Preliminary User'Manual February 28, 1973
(2) Editing Strategies.
Editing strategies are applied to the resluts of the rules of
inference. These strategies are used to filter out some of the
deductions which a rule of inference has generated.
Builtin editing strategies.
a) DEMOD is a rule of simplification most commonly used in
conjunction with EQUALITY. DEMOD takes two arguments. The first
describes a list of equality units; the second, a number named DDEPTH
which,like PDEPTH, determines a bound on the matching routines.
b) DEPTH takes a single integer argument interpreted to be a bound on
the depth of function symbol nesting which must not be exceeded if
the deduction is to be retained.
For example, DEPTH[4].
c) LENGTH also takes an integer argument and gives a bound on the
number of literals which will be allowed in any deduction.
Preliminary User'Manual February 28, 1973
Boolean combinations of built-in or user-defined strategies are
allowed. For example, a reasonable choice strategy is: ancestry
filter form with a set of support being the negation of the statement
to be proved. This can be written as:
ANCESTRY ∧ SUPPORT[THEOREM];
An editing strategy which filters out all clauses whose length(number
of literals) is greater than 4 or whose depth( depth of nesting of
function symbols) is greater than 3 can be expressed as:
LENGTH[4] ∨ DEPTH [3];
Preliminary User'Manual February 28, 1973
A programmable theorem prover.
It is now possible to write LISP-like programs which control the
actions of the theroem prover and manipulate clauses. Data types
for CLAUSES, STRATEGIES, and PATTERNS have been added to LISP so that
the user can describe his clause manipulations in the same notation
which is used to drive the on-line prover. LISP functions, TRYTIL
and FIND, have been defined to perform controlled proof-attempts and
clause-list searching.
1. Data Types.
a) [CLAUSES <clauses>] is used to introduce new clause lists to the
program. For example: (SETQ X [CLAUSES DSK:FOO]) when executed will
assign to X the clauselist manufactured from the statements on file
FOO.
b) [CHOICE <strategy>] and [EDIT <strategy>] introduce the
appropriate strategies.
c) [PATTERN <pattern>] is useful in conjunction with FIND to filter
out clauses which match <pattern>.
2. Procedures.
(TRYTIL <clauses><choice-strategy><edit-strategy><termination
condition>)
where: 1) <clauses> is a list of clauses . 2) <choice-strategy> is a
representation of a choice strategy. 3) <edit-strategy> represents
an editing strategy. 4) <termination condition> is a functional
Preliminary User'Manual February 28, 1973
argument which will be evaluated periodically during the execution of
the TRYTIL. As long as the condition evaluated to NIL the proof
attempt will continue. If the condition becomes true then TRYTIL will
return the list of all deductions which have been made.
For example:
(TRYTIL [CLAUSES DSK: FOO] [CHOICE ANCESTRY∧SUPPORT[THEOREM]] [EDIT
LENGTH[4]∨DEPTH[3]] (FUNCTION (LAMBDA()(GREATERP LEVEL 3))) )
will begin a proof search using file DSK:FOO with choice strategy
being AFF and supporting the negation of the theorem. Deductions
whose length is greater than 4 or whose depth of fuction nesting is
greater than 3 will be discarded. The proof search will terminate at
the end of level 3.
If a refutation is discovered during any attempt, (QED) is returned.
If no retutation is found, then the on-line editor is called to give
the user a chance to examine the current proof environment. There is
a third way to exit TRYTIL: since the on-line editor is available
inside the proof attempt, typing ABandon <clauses> to the editor
will force termination of the proof attempt and will return the
selected <clauses>.
(FIND <clauses><pattern>)
where: 1) <clauses> is a list of clauses. 2) <pattern> is a
condition which is to be applied to each element of <clauses>.
The value of FIND is a list of all elements of <clauses> which
satisfy the <pattern>.
Preliminary User'Manual February 28, 1973
For example (FIND XX [PATTERN α(C)=1]) will find all clauses in XX
which are units(singletons).
The parsers for the input syntax and the command language are both
contstructed by Lynn Quam's Syntax Directed Input Output program.
Preliminary User'Manual February 28, 1973
THE SIMPLE STRATEGY LANGUAGE
The most straightforwrd application of the strategy language consists
of using Boolean combinations of the builtin strategies.
<STRATEGY>::=<F1>;
<F1> ::=<F2>
::=<F1><OR><F2>
<F2> ::=<F3>
::=<F2><AND><F3>
<F3> ::=(<F1>)
::=<NOT><F3>
::=<PREDIC>
<PREDIC>::=ANCESTRY
::=NONE
::=VINE
::=UNIT
::=P1
::=SUPPORT[<C>]
::=MODEL[<PREDLST>;<PREDLST>]
::=EQUALITY[<OP>,<NUMBER>]
::=DEMOD[<CLAUSES>,<NUMBER>]
::=DEFMODEL[ID]
::=LENGTH[<NUMBER>]
::=DEPTH[<NUMBER>]
<PREDLST>
::=<ID>,<PREDLST>
::=<ID>
::=
Preliminary User'Manual February 28, 1973
THE INPUT FORMAT
The usual form for input consists of the declarations of the non-
logical constituents of the axioms, followed by a sequence of
statements. The statements may be assigned names, and if a statement
named THEOREM is present that statement is negated before being added
to the memory of the prover.
<INPUT> ::=<DECOP>:<OPLIST>;
::=<ID>:
::=<S>
<DECOP> ::=VAR | INF_OP | INF_PRED | PRE_OP | PRE_PRED | EQUALITY
<OPLIST>::=<OP>,<OPLIST>
::=<OP>
<S> ::=;
::=<S1>;
<S1> ::=<S2>
::=<S1><EQUIV><S2>
<S2> ::=<S3>
::=<S2><IMP><S3>
<S3> ::=<S4>
::=<S3><OR><S4>
<S4> ::=<S5>
::=<S4><AND><S5>
<S5> ::=(<S1>)
::=<NOT><S5>
::=<QFF><BODY>
::=<PRED>
<BODY> ::= <IVAR><S5>
::=(<VARLIST>)<S5>
<VARLIST>::=<IVAR>,<VARLIST>
::=<IVAR>
Preliminary User'Manual February 28, 1973
In the following,the routines corresponding to <PREPREDLET>,
<INFPREDLET>, <IVAR>, <PREFN>, and <INFN> check the lists of prefix-
and infix- predicate and function letters, and the variable list, all
of which were manufactured by the appropriate declarations.
<PRED> ::=<PREPREDLET><ITMLST>
::=<TM><INFPREDLET><TM>
<ITMLST>::=(<ITMS>)
<ITMS> ::=<TM><ITMS>
::=<TM>
<TM> ::=<IVAR>
::=<PREFN><ITMLST>
::=<PREFN>
::=(<TM>)
::=<TM><INFN><TM>
The logical connectives are defined as follows:
<EQUIV> ::= ≡ | ↔
<IMP> ::= ⊃
<OR> ::= ∨
<AND> ::= ∧
<NOT> ::= ¬
<QFF> ::= ∀ | ∃